    
:- use_module(library(timeout)).



r5_drop([], D, D) :- 
    !.
r5_drop([[I-t,C-t] | Rest], D, Res) :- 
    member(node(C, _, _, CR), D),		   
    del(node(I, Lit, C, R), D, D1),
    insert(node(I, Lit, CR, R), D1, D2),
    r5_drop(Rest, D2, Res),
    !.	     
r5_drop([[I-t,C-f] | Rest], D, Res) :- 
    member(node(C, _, CL, _), D),		   
    del(node(I, Lit, C, R), D, D1),
    insert(node(I, Lit, CL, R), D1, D2),
    r5_drop(Rest, D2, Res),
    !.	     
r5_drop([[I-f,C-t] | Rest], D, Res) :- 
    member(node(C, _, _, CR), D),		   
    del(node(I, Lit, L, C), D, D1),
    insert(node(I, Lit, L, CR), D1, D2),
    r5_drop(Rest, D2, Res),
    !.	     
r5_drop([[I-f,C-f] | Rest], D, Res) :- 
    member(node(C, _, CL, _), D),		   
    del(node(I, Lit, L, C), D, D1),
    insert(node(I, Lit, L, CL), D1, D2),
    r5_drop(Rest, D2, Res).	     




r5([], Edges, Edges) :- 
    !.
r5([path(_,_,PathEdges,Path) | Rest], EdgesSoFar, Edges) :- 			     
%    time_out((implication(Path, [false]), A = 1 ; A = 0), 1000, Res),    
%    !, 
%    (once((A == 1)), 
%     Res == success,
%     batchInsert(PathEdges, EdgesSoFar, EdgesSoFar1)
%     ;
%     EdgesSoFar1 = EdgesSoFar),
%      write(Path), write(': '),
      getBasicBkgd(Path, [], Objs, ExPath1), 
      floodState(ExPath1, Objs, ExPath),
      !,
      (not(member(false, ExPath)),
       !,
%       write('Safe'), nl, 
       get_edge_pairs(PathEdges, PathEdgePairs),
       diff(EdgesSoFar, PathEdgePairs, EdgesSoFar1)
       ;
%       write('XXX'), nl, 
       EdgesSoFar1 = EdgesSoFar), 
    !,
    r5(Rest, EdgesSoFar1, Edges).
      	



r5(D, Res) :-
    get_all_edge_pairs(D, AllEdges),
    (debug(r5) -> write('All edges'), write(AllEdges), nl ; true),
%    write(AllEdges),nl,
    D = [node(Root, _, _, _) | _],    
    get_all_paths(Root, D, [], [], Paths),
    r5(Paths, AllEdges, Edges),
%    write(Edges), nl, 
%    diff(AllEdges, Edges, EdgesToRemove),
%    write(EdgesToRemove),nl,
     !,
    r5_drop(Edges, D, Res).
    


      




    
%% r8(+, -)
%% r8(D, R)
%% True when R is the result of applying the equality reduction to the root node of FODD D. Only the root node is chosen to avoid cases where nodes/subFODDs have to be split etc. The procedure works as follows. The first check is to see that the root node is an equality node eq(X, Y), otherwise this reduction is not applicable. Then we check to see that atleast one of the X and Y is a domain variable, otherwise r8 is not applicable. Then come the r8 conditions, namely that the right subFODD of the root does not contain both X and Y. If, this is satisfied then we proceed. Now variable replacements have to be made depending on which variable is present on the right subFODD of the root. The variable to replace X and/or Y with is generated by the getReplVar(+, +, -) procedure found in the file reductionUtils.pl. Finally the root is chopped off and the left and right subFODDs are combined with the max procedure. 

r8(D, Res) :- 
    D = [node(_, eq(X, Y), L, R) | _],

%%%%%%%%%%% check for r8 condition that X and Y cannot both appear on the right subFODD %%%%%%%%%%%%
%%%%%%%%%%% of the root and atleast one of them has to be adomain variable. %%%%%%%%%%%%%%%%%%%%%%%

    (domVar(X) ; domVar(Y)),
    getSubDD(R, D, RD),
    getDVarsConsts(RD, [], Vars), 
    not((member(X, Vars), member(Y, Vars))),
    (debug(6) -> write('r8 applicable'), nl ; true),

%%%%%%%%%% Finding the replacement variables for X and/or Y %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

    (not(member(Y, Vars)),
     domVar(Y),
%     write('r8 case 1'), nl, 
     (debug(6) -> write(Y), write(' to be replaced by '), write(X), nl ; true),
     getReplVar(D, [Y, X], ReplVar),
     (debug(6) -> write('Repl Var: '), write(ReplVar), nl ; true),
     (ReplVar = X -> Key = [Y:ReplVar] ; Key = [X:ReplVar, Y:ReplVar]),
     replaceDVars(D, Key, D1)
     ;
     not(member(X, Vars)),
     domVar(X),
%     write('r8 case 2'), nl, 
     (debug(6) -> write(X), write(' to be replaced by '), write(Y), nl ; true),
     getReplVar(D, [X, Y], ReplVar),
     (debug(6) -> write('Repl Var: '), write(ReplVar), nl ; true),
     (ReplVar = X -> Key = [X:ReplVar] ; Key = [X:ReplVar, Y:ReplVar]),
     replaceDVars(D, Key, D1)),

%%%%%%%%%% Perform the max %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

    member(node(L, LLit, LL, LR), D1),
    member(node(R, RLit, RL, RR), D1),    
    apply(node(L, LLit, LL, LR), D1, node(R, RLit, RL, RR), D1, max, D2),
    r8(D2, Res),
    !.
r8(D, D).





%% r81(+, -)
%% r81(D, R)
%% True when R is the result of applying the equality reduction to the root node of FODD D. Only the root node is chosen to avoid cases where nodes/subFODDs have to be split etc. The procedure works as follows. The first check is to see that the root node is an equality node eq(X, Y), otherwise this reduction is not applicable. Then we check to see that atleast one of the X and Y is a domain variable, otherwise r8 is not applicable. Then come the r8 conditions, namely that the right subFODD of the root does not contain both X and Y. If, this is satisfied then we proceed. Now variable replacements have to be made depending on which variable is present on the right subFODD of the root. The variable to replace X and/or Y with is generated by the getReplVar(+, +, -) procedure found in the file reductionUtils.pl. Finally the root is chopped off and the left and right subFODDs are combined with the max procedure. 

r81(D, Res) :- 
    r9on,
%    once(length(D, DLen)),
    once(D = [node(Root, _, _, _) | _]),
    member(node(I, eq(X, Y), L, R), D),

%%%%%%%%%%% check for r8 condition that X and Y cannot both appear on the right subFODD %%%%%%%%%%%%
%%%%%%%%%%% of the root and atleast one of them has to be adomain variable. %%%%%%%%%%%%%%%%%%%%%%%

    once((domVar(X) ; domVar(Y))),
    once(getSubDD(R, D, BnR)),
    (debug(g) -> write('BnR obtained'), nl ; true),
    once(getDVarsConsts(BnR, [], Vars)),
    once(not((member(X, Vars), member(Y, Vars)))),
    (debug(6) -> write('r81 applicable on '), write(I), nl ; true),
    
%%%%%%%%%% Finding the replacement variables for X and/or Y %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
    
    (once(not(member(Y, Vars))),
    once(domVar(Y)),
    once(collectNodeFormula(I, D, NF)),
    once(getNFVars(NF, [], NFVars)),
    once(not(member(Y, NFVars))),
    (debug(6) -> write('r81 case 1'), nl ; true), 
    (debug(6) -> write(Y), write(' to be replaced by '), write(X), nl ; true),
    once(getSubDD(L, D, BnL)),
%    write(getReplVar(D, BnL, [Y, X], ReplVar)),
    (debug(6) -> write('entering getReplVar'), nl ; true),
    getReplVar(D, BnL, [Y, X], ReplVar),
    (debug(6) -> write('Repl Var: '), write(ReplVar), nl ; true),
    once((ReplVar == X -> (getGroundKey([Y], [X], Key), replaceDVars(BnL, Key, BnLp), BnRp = BnR, D1 = D) 
	  ; 
	  getGroundKey([Y, X], [ReplVar, ReplVar], Key1),
	  getGroundKey([X], [ReplVar], Key2),
	  replaceDVars(BnL, Key1, BnLp), replaceDVars(BnR, Key2, BnRp), replaceDVars(D, Key2, D1)))
    ;
    once(not(member(X, Vars))),
    (debug(6) -> write('not member X Vars'), nl ; true),
    once(domVar(X)),
    once(collectNodeFormula(I, D, NF)),
    once(getNFVars(NF, [], NFVars)),
    once(not(member(X, NFVars))),
    (debug(6) -> write('r81 case 2'), nl ; true),
    (debug(6) -> write(X), write(' to be replaced by '), write(Y), nl ; true),
    once(getSubDD(L, D, BnL)),
    (debug(6) -> write('BnL obtained'), nl ; true),
    once(getReplVar(D, BnL, [X, Y], ReplVar)),
    (debug(6) -> write('Repl Var: '), write(ReplVar), nl ; true),
    once((ReplVar == Y -> getGroundKey([X], [Y], Key), replaceDVars(BnL, Key, BnLp), BnRp = BnR, D1 = D 
	  ; 
	  getGroundKey([Y, X], [ReplVar, ReplVar], Key1),
	  getGroundKey([Y], [ReplVar], Key2),
	  replaceDVars(BnL, [Y:ReplVar, X:ReplVar], BnLp), replaceDVars(BnR, [Y:ReplVar], BnRp), replaceDVars(D, [Y:ReplVar], D1)))),
    
%%%%%%%%%% Perform the max %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

    retractall(nf3579(_, _)),
	  BnLp = [BnLpRoot | _],
	  BnRp = [BnRpRoot | _],
	  apply(BnLpRoot, BnLp, BnRpRoot, BnRp, max, Bnp),
	  (debug(6) -> write('Bnp: '), write(Bnp), nl ; true),
	  (I == Root -> D3 = Bnp
	   ;
	   insert(node(0, 0.0, -1, -1), D1, D0),
	   parentUpdate(D0, 0, I, D2a, _),
	   removeUnreachable(Root, [I], D2a, Ba, _),
	   (debug(6) -> write('Ba: '), write(Ba), nl ; true),
	   getLeafIndices(D1, LeafIndices),
	   batchParentUpdate(D0, 0, LeafIndices, D3b, PL),
	   insert(node(1, 1.0, -1, -1), D3b, D4b),
	   parentUpdate(D4b, 1, I, D5b, _),     
	   r1r2Cycle(PL, D5b, Bb),
	   (debug(6) -> write('Bb: '), write(Bb), nl ; true),
	   Ba = [BaRoot | _],
	   Bb = [BbRoot | _],
	   Bnp = [BnpRoot | _],
%          write(apply(BnpRoot, Bnp, BbRoot, Bb, *, Bnbp)), nl, 
	   apply(BnpRoot, Bnp, BbRoot, Bb, *, Bnbp), 
	   (debug(6) -> write('Bnbp: '), write(Bnbp), nl ; true),
	   Bnbp = [BnbpRoot | _],
	   apply(BnbpRoot, Bnbp, BaRoot, Ba, +, D3)),
%	  length(D3, D3Len))),
%    D3Len < DLen,
    (debug(6) -> write('r81 gives: '), write(D3), nl ; true),
    r81(D3, Res),
    !.
r81(D, D).
    









replace_edge_target([], _, []) :- 
    !.
replace_edge_target([node(I, Lit, L, R) | Rest], Edges, [node(I, Lit, 0, R) | Rest1]) :-
    member(I-t, Edges),
    replace_edge_target(Rest, Edges, Rest1),
    !.
replace_edge_target([node(I, Lit, L, R) | Rest], Edges, [node(I, Lit, L, 0) | Rest1]) :-
    member(I-f, Edges),
    replace_edge_target(Rest, Edges, Rest1),
    !.
replace_edge_target([Node | Rest], Edges, [Node | Rest1]) :-
    replace_edge_target(Rest, Edges, Rest1).		  







perform_r9([], [], _, Edges, _, Edges) :-
    !.
perform_r9([path(N, _, GPEdges, GroundPath) | GroundRestPaths], [_ | RestPaths], HigherPaths, EdgesSoFar, Dir, Edges) :-
    once(my_intersection(GPEdges, EdgesSoFar, CommEdges)),
    CommEdges \== [],
    once(getBasicBkgd(GroundPath, [], Objs, ExPath1)),
    (debug(1) -> nl, write('Bkgd Collected '), nl ; true),
    once(floodState(ExPath1, Objs, ExPath)),
%    once(GroundPath = [FirstLit | AfterPath]),
    (debug(1) -> write('State Flooded '), nl ; true),
    (not(pathSatisfiable(ExPath, ExPath))
     ;
     member(path(HN, _, _, Path), HigherPaths),    
%    once(interpretPath(Path, Path1)),
    once(HNDir is HN * Dir),
    once(NDir is N * Dir),
    NDir = HNDir,
    (debug(1) -> nl, write('GroundPath = '), write(GroundPath), nl ; true),    
    (debug(1) -> write('Path = '), write(Path), nl ; true),
    not(not(subsumes1(Path, ExPath)))),
    (debug(1) -> write('proved'), nl ; true),
    perform_r9(GroundRestPaths, RestPaths, HigherPaths, EdgesSoFar, Dir, Edges),
    !.
perform_r9([path(_, _, EdgeList, _) | GroundRestPaths], [HP | RestPaths], HigherPaths, EdgesSoFar, Dir, Edges) :-
    (debug(1) -> write('EdgeList: '), write(EdgeList), nl ; true),
    (debug(1) -> write('EdgesSoFar: '), write(EdgesSoFar), nl ; true),
    diff(EdgesSoFar, EdgeList, EdgesSoFar1),
    (debug(1) -> write('EdgesSoFar1: '), write(EdgesSoFar1), nl ; true),
    conc(HigherPaths, [HP], HigherPaths1),
%    HigherPaths1 = [HP | HigherPaths],
    perform_r9(GroundRestPaths, RestPaths, HigherPaths1, EdgesSoFar1, Dir, Edges).

    





r9(D, R) :-
    D = [node(Root, _, _, _) | _],
    get_all_edges(D, AllEdges),
    (debug(1) -> write('All edges'), write(AllEdges), nl ; true),
    get_paths(Root, D, [], [], GroundPaths1),
    length(GroundPaths1, LenGP1),
    (debug(1) -> write('Collected Ground Paths of length '), write(LenGP1), nl ; true),
    insertsort(GroundPaths1, GroundPaths),
    (debug(1) -> write('Sorted Ground Paths: '), nl, write(GroundPaths), nl ; true),
    getDVars(D, Vars),
    getSubsKey(Vars, Key),
    variablizeDD(D, Key, DVar),
    (debug(1) -> write('Variablized D'), nl ; true),
    get_paths(Root, DVar, [], [], Paths1),
    length(Paths1, LenP1),
    (debug(1) -> write('Collected Variablized Paths of length '), write(LenP1), nl ; true),
    insertsort(Paths1, Paths),
    (debug(1) -> write('Sorted Variablized Paths: '), nl, write(Paths), nl ; true),
    perform_r9(GroundPaths, Paths, [], AllEdges, 0, Edges),
    (debug(1) -> write('r9 performed: '), write(Edges), nl ; true),
    ((Edges = [] ; member(node(0, 0.0, -1, -1), D)), D0 = D ;  insert(node(0, 0.0, -1, -1), D, D0)),
    replace_edge_target(D0, Edges, D1, [], HL1),
    (debug(1) -> write('Target Edge Replaced, HL1 = '), write(HL1), nl ; true),
    insertsort(HL1, HL2),
    (debug(1) -> write('Sorted HL2 = '), write(HL2), nl ; true),
    removeUnreachable(_, HL2, D1, D2, HL3), 
    (debug(1) -> write('Unreachable Removed'), nl ; true),
%    r5(HL3, D2, R).
    (Edges = [],
     R = D2
     ;
     once(eraseBatchNF(Edges, D)),
    once(eraseBatchSuperss(Edges, D)),
    (debug(1) -> write('calling drop cycle'), nl ; true),
%    write('calling drop cycle'), nl,
     once(r9_drop_cycle(Edges, D2, HL3, D3)),
%    write('returning from drop cycle'), nl,
    (debug(1) -> write('returning from drop cycle'), nl ; true),
     (D3 = D2,
      R = D3
      ;
      r9(D3, R))).
    
    




r92(D, R) :-
    D = [node(Root, _, _, _) | _],
    get_all_edges(D, AllEdges),
    (debug(1) -> write('2 All edges '), write(AllEdges), nl ; true),
    get_paths_rev(Root, D, [], [], GroundPaths1),
    length(GroundPaths1, LenGP1),
    (debug(1) -> write('2 Collected Ground Paths of length '), write(LenGP1), nl ; true),
    sort(GroundPaths1, GroundPaths),
    (debug(1) -> write('2 Sorted Ground Paths: '), nl, write(GroundPaths), nl ; true),
    getDVars(D, Vars),
    getSubsKey(Vars, Key),
    variablizeDD(D, Key, DVar),
    (debug(1) -> write('2 Variablized D'), nl ; true),
    get_paths_rev(Root, DVar, [], [], Paths1),
    length(Paths1, LenP1),
    (debug(1) -> write('2 Collected Variablized Paths of length '), write(LenP1), nl ; true),
    sort(Paths1, Paths),
    (debug(1) -> write('2 Sorted Variablized Paths: '), nl, write(Paths), nl ; true),
    perform_r9(GroundPaths, Paths, [], AllEdges, 1, Edges),
    (debug(1) -> write('2 r9 performed: '), write(Edges), nl ; true),
    ((Edges = [] ; member(node(0, 0.0, -1, -1), D)), D0 = D ;  insert(node(0, 0.0, -1, -1), D, D0)),
    replace_edge_target(D0, Edges, D1, [], HL1),
    (debug(1) -> write('2 Target Edge Replaced, HL1 = '), write(HL1), nl ; true),
    insertsort(HL1, HL2),
    removeUnreachable(_, HL2, D1, D2, HL3), 
    (debug(1) -> write('2 Unreachable Removed HL3 = '), write(HL3), nl ; true),
%    r5(HL3, D2, R).
    (Edges = [],
     R = D2
     ;
     once(eraseBatchNF(Edges, D)),
     once(eraseBatchSuperss(Edges, D)),
    (debug(1) -> write('2 calling drop cycle'), nl ; true),
     once(r9_drop_cycle(Edges, D2, HL3, D3)),
    (debug(1) -> write('2 returning from drop cycle'), nl ; true),
     (D3 = D2,
      R = D3
      ;
      r92(D3, R))).



    

r9_drop([], D, _, [], [], D) :-
%    r5(ReplRem, D, Res),
    !.
r9_drop([I2-E2 | Rest], D, DVars, ReplRem, Rem, Res) :-
    once(domainConsts(DomConsts)),
    once(conc(DomConsts, DVars, QVars)),
    once(member(node(I2, Lit2temp, L2, R2), D)),
    once((E2 = t,
     Lit2 = Lit2temp,
     C2sib = R2
     ;
     getNeg(Lit2temp, Lit2),
     C2sib = L2)),
    once(collectNodeFormula(I2, D, NF2)),
    once(EF2 = [Lit2 | NF2]),
    once(all(ExPath, (get_a_path(EF2, [], Path), once((getBasicBkgd(Path, QVars, Objs, ExPath1), floodState(ExPath1, Objs, ExPath)))), ExPaths)),
    member(node(I1, Lit1, L1, R1), D),
    once(L1 \= -1),
%    once(getNeg(Lit1temp, NLit1temp)),
    member([Lit1, C1, E1], [[Lit1temp, L1, t], [NLit1temp, R1, f]]),
    once(member(node(C1, CLit1, CL1, CR1), D)),
    once(member(node(C2sib, CLit2sib, CL2sib, CR2sib), D)),

    (debug(1) -> write('I1 = '), write(I1), write(' I2 = '), write(I2), write(' E1 = '), write(E1), write(' E2 = '), write(E2), nl ; true),
    (debug(1) -> write('C1 = '), write(C1), write(' C2sib = '), write(C2sib), nl ; true),  
    once(superSub(node(C1, CLit1, CL1, CR1), D, node(C2sib, CLit2sib, CL2sib, CR2sib), D, Vsib)),     
%    write('atleast'), nl, 
   

    once((reach3579(I1, E1, I2, E2, Vsib, Tsib)
          ;
          once(getEdgeFormula1(edge(I1, Lit1, E1), D, Vsib, EF1sib)),           
	  (debug(1) -> write('ExPaths: '), write(ExPaths), nl ; true),
	  (debug(1) -> write('EF1sib = '), write(EF1sib), nl ; true),
    
	  (prove_all(ExPaths, EF1sib), Tsib = 1 ; Tsib = 0),
          once(asserta(reach3579(I1, E1, I2, E2, Vsib, Tsib))))),    
%    write('Tsib = '), write(Tsib), nl,
    Tsib = 1,
    (debug(1) -> write('drop proved'), nl ; true),
    parentUpdate(D, C2sib, I2, D1, Par),
    del(node(I2, _, _, _), D1, D2),
    eraseSubDDNF(I2, D),
%    retractall(nf3579(_, _)), 
    eraseSuperss(I2, D),
    
    r9_drop(Rest, D2, DVars, ReplRem1, Rem, Res),
    insert(C2sib, ReplRem1, ReplRem),
    !.
r9_drop([X | Rest], D, DVars, ReplRem, Rem, Res) :-    
    r9_drop(Rest, D, DVars, ReplRem, Rem1, Res),
    insert(X, Rem1, Rem).

    
    
    
r9_drop_cycle(EdgeList, D, ReplRem, Res) :-
    (debug(1) -> nl, write('drop cycle entered'), nl ; true), 
    getDVars(D, DVars),
%    write('drop cycle entered'), nl, write(D), nl, write(r9_drop(EdgeList, _, DVars, HL, Rem, R)), nl, 
    r9_drop(EdgeList, D, DVars, HL, Rem, R),
%    write('Rem = '), write(Rem), nl, 
    batchInsert(HL, ReplRem, HL1),
    (debug(1) -> write('Rem = '), write(Rem), write(' HL = '), write(HL), nl ; true),
    (D = R,
     !,
%     write('doing r5'), nl,  
     r5(HL1, R, Res),
%     write('back from r5 after r9-drop: '), write(Res), nl,
     (debug(1) -> write('back from r5 after r9-drop: '), write(Res), nl, pp(Res), nl ; true)
     ;
     r9_drop_cycle(Rem, R, HL1, Res)).





    
r10([node(_, eq(_, _), _, 0) | Rest], Res) :-
    r10(Rest, Res),
    !.
r10([node(_, eq(_, _), 0, _) | Rest], Res) :-
    r10(Rest, Res), 
    !.
r10(D, Res) :-
    del(node(I, eq(_, _), 0, R), D, D1),
    parentUpdate(D1, R, I, D2),
    r10(D2, Res),
    !.
r10(D, Res) :-
    del(node(I, eq(_, _), L, 0), D, D1),
    parentUpdate(D1, L, I, D2),
    r10(D2, Res),
    !.
r10(D, D).    






r11([], D, _, D) :-
    retractall(nf3579(_, _)),
    !.
r11([node(I, Lit, 0, R) | Candidates], D, Key, Res) :-
    once(getNeg(Lit, NLit)),
    once(collectNodeFormula(I, D, NF)),    
    once(get_paths(R, D, [], [], Paths)),
    once(all(Path, (get_a_disjunct(NF, [], SuperPath), member(path(_, _, _, SubPath), Paths), conc(SuperPath, SubPath, Path)), AllPaths)),
    once(length(AllPaths, Len)),
%    write('AllPaths: '), write(AllPaths), nl, 
    once(findall(1, (member(P, AllPaths), once((variablizeFormula([NLit | P], Key, VarP), getBasicBkgd([Lit | P], [], Objs, ExPath1), floodState(ExPath1, Objs, ExPath))), once(subsumes2(VarP, ExPath))), Z)),
%    write('Z: '), write(Z), nl, 
    length(Z, Len),
%    write(node(I, Lit, 0, R)), write('removed'), nl,
    del(node(I, Lit, 0, R), D, D1),
    parentUpdate(D1, R, I, D2, _),
%    write('Parent Updated'), nl, 
    retractall(nf3579(_, _)),
    r11(Candidates, D2, Key, Res),
    !.
r11([node(I, Lit, L, 0) | Candidates], D, Key, Res) :-
    once(getNeg(Lit, NLit)),
    once(collectNodeFormula(I, D, NF)),    
%    write(NF), nl, 
    once(get_paths(L, D, [], [], Paths)),
    once(all(Path, (get_a_disjunct(NF, [], SuperPath), member(path(_, _, _, SubPath), Paths), conc(SuperPath, SubPath, Path)), AllPaths)),
    once(length(AllPaths, Len)),
%    write('AllPaths: '), write(AllPaths), nl, 
    once(findall(1, (member(P, AllPaths), once((variablizeFormula([Lit | P], Key, VarP), getBasicBkgd([NLit | P], [], Objs, ExPath1), floodState(ExPath1, Objs, ExPath))), once(subsumes2(VarP, ExPath))), Z)),
%    write('Z: '), write(Z), nl, 
    length(Z, Len),
%    write(node(I, Lit, L, 0)), write('removed'), nl, 
    del(node(I, Lit, L, 0), D, D1),    
    parentUpdate(D1, L, I, D2, _), 
%    write('parent Updated'), nl, 
    retractall(nf3579(_, _)),
    r11(Candidates, D2, Key, Res),    
    !.    
r11([_ | Candidates], D, Key, Res) :-
    r11(Candidates, D, Key, Res).
    

r11(D, Res) :-
    r11on,
    !,
    getDVars(D, Vars),
    getSubsKey(Vars, Key),
    (all(node(I, eq(X, Y), L, 0), member(node(I, eq(X, Y), L, 0), D), CandEqL) ; CandEqL = []),
    (all(node(I, eq(X, Y), 0, R), member(node(I, eq(X, Y), 0, R), D), CandEqR) ; CandEqR = []),
    (all(node(I, Lit, 0, R), (member(node(I, Lit, 0, R), D), once((Lit =.. [P | _], not(P = eq), member(node(R, LitR, _, _), D))), LitR =.. [P | _]), CandR) ; CandR = []), 
    (all(node(I, Lit, L, 0), (member(node(I, Lit, L, 0), D), once((Lit =.. [P | _], not(P = eq), member(node(L, LitL, _, _), D))), LitL =.. [P | _]), CandL) ; CandL = []), 
    flatten([CandL, CandR, CandEqL, CandEqR], Candidates),
%    write('Candidates: '), write(Candidates), nl,
    r11(Candidates, D, Key, Res),
    !.
r11(D, D).
    
